COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 know.lsp[w84,jmc]	ekl axioms
C00004 ENDMK
C⊗;
;;; know.lsp[w84,jmc]	ekl axioms

(decl (p q r) (type: ground) (sort: prop))
(decl (S) (type: ground) (sort: person))
(decl (istrue) (type: |ground→truthval|) (syntype: constant))
(decl (and) (type: |ground*→ground|) (syntype: constant) (infixname: and))
(decl (or) (type: |ground*→ground|) (syntype: constant) (infixname: or))
(decl not (type: |ground → ground|) (syntype: constant))
(decl implies (type: |ground⊗ground→ground|) (syntype: constant)
      (infixname: implies))
(decl fool (type: ground) (sort: person) (syntype: constant))
(decl join (type: |ground* → ground|) (syntype: constant) (infixname: join))

(axiom |∀p q.istrue(p and q) ≡ istrue p ∧ istrue q|)
(label simpinfo)
(axiom |∀p q.istrue(p or q) ≡ istrue p ∨ istrue q|)
(label simpinfo)
(axiom |∀p q.istrue(p implies q) ≡ (istrue p ⊃ istrue q)|)
(label simpinfo)
(axiom |∀p.istrue(not p) ≡ ¬(istrue p)|)
(label simpinfo)

(decl knows (type: |ground⊗ground→ground|) (syntype: constant) (infixname: *))
;;;
(derive |∀p.istrue(p or (not p))| 11 13)
(derive |∀p.istrue(p implies p)| 12)
(trw |∀p.istrue(p implies p)| 12)
(show 1:*)
(trw |∀p.istrue(p implies p)| (use 12 ue: ((p.p)(q.p))))
(ue ((p.p)(q.p)) 12)